•    Множество уравнений, известных как правила перезаписи (rewrites), или демодуляторы (demodulators). Хотя демодуляторы представляют собой уравнения, они всегда применяются в направлении слева направо, поэтому определяют каноническую форму, в которой должны быть представлены все упрощенные термы. Например, демодулятор х+0=х указывает, что любой терм в форме х+0 должен быть заменен термом х.

•    Множество параметров и выражений, который определяет стратегию управления. В частности, пользователь задает эвристическую функцию для управления поиском и функцию фильтрации для устранения некоторых подцелей как не представляющих интереса.

Программа Otter действует по принципу постоянного применения правила резолюции к одному из элементов множества поддержки и к одной из полезных аксиом. В отличие от системы Prolog, в этой программе используется определенная форма поиска по первому наилучшему совпадению. Ее эвристическая функция измеряет "вес" каждого выражения с учетом того, что наиболее предпочтительными являются выражения с наименьшими весами. Задача точной формулировки эвристической функции возлагается на пользователя, но, вообще говоря, вес любого выражения должен коррелировать с его размером или сложностью. Единичные выражения оцениваются как имеющие наименьший вес, поэтому такой метод поиска может рассматриваться как обобщение стратегии с преимущественным использованием единичных выражений. На каждом этапе программа Otter перемещает выражение "с наименьшим весом" из множества поддержки в список полезных аксиом и добавляет в множество поддержки некоторые непосредственные следствия применения операции резолюции к выражению с наименьшим весом и к элементам списка полезных аксиом. Программа Otter останавливается, если обнаруживает противоречие или если возникает такая ситуация, что в множестве поддержки не остается больше выражений. Алгоритм работы этой программы показан более подробно в листинге 9.5.

Листинг 9.5. Набросок структуры программы автоматического доказательства теорем Otter. Эвристическое управление применяется при выборе выражения "с наименьшим весом" и в функции Filter, которая устраняет из рассмотрения такие выражения, которые не представляют интереса

<< В начало < Предыдущая 1 2 3 4 5 6 Следующая > В конец >>